『Cubical Type Theory: a constructive interpretation of the univalence axiom』

1. どんなもの？

2. 先行研究と比べてどこがすごい？

3. 技術や手法のキモはどこ？

4. どうやって有効だと検証した？

5. 議論はある？

6. 次に読むべき論文は？

table:訳

cubical type theory 立方型理論

free bounded distributive lattice 自由有界分配束

antichain 反鎖

join irreducible element 結び非分解要素？

face lattice 面束

de Morgan algebra ド・モルガン代数

absorption law 吸収則

context 文脈

substitution 代入

beta-conversion ベータ変換

eta-conversion エータ変換

function extensionality 関数外延性

path type 道型

partial element 部分要素

composition operation 合成操作

sigma type シグマ型

product type 積型

sum type 和型

equivalence 同値

contractible 可縮

glueing 接着

transport function 輸送関数

dependent type 依存型

path equal 道等値

universe 宇宙

univalence ユニバレンス、一価の？